Left Termination of the query pattern
mult(g,g,a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

mult(X1, 0, 0).
mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z)).
sum(X, 0, X).
sum(X, s(Y), s(Z)) :- sum(X, Y, Z).

Query: mult(g,g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: mult(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: mult(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | mult(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | mult(T5, 0, T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: mult(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nX3 is free\nmult(T1, T2, T3) !=? mult(X3, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: mult(T5, 0, T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(mult(T10, T11, X13), sum(X13, T10, T13))\n\nT10 is ground\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 0 | ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 1\n\nT10 is ground\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 0\n\nT10 is ground\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 1\n\nT10 is ground\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: sum(0, T18, T13)\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: sum(0, T18, T13), SCOPE: 3, CLAUSE: 2 | sum(0, T18, T13), SCOPE: 3, CLAUSE: 3\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: sum(0, T18, T13), SCOPE: 3, CLAUSE: 2\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: sum(0, T18, T13), SCOPE: 3, CLAUSE: 3\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: sum(0, T23, T25)\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(','(mult(T30, T31, X49), sum(X49, T30, X50)), sum(X50, T30, T13))\n\nT30 is ground\nT31 is ground\nX50 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: mult(T30, T31, X49)\n\nT30 is ground\nT31 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(sum(T34, T30, X50), sum(X50, T30, T13))\n\nT30 is ground\nT34 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: mult(T30, T31, X49), SCOPE: 4, CLAUSE: 0 | mult(T30, T31, X49), SCOPE: 4, CLAUSE: 1\n\nT30 is ground\nT31 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: mult(T30, T31, X49), SCOPE: 4, CLAUSE: 0\n\nT30 is ground\nT31 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: mult(T30, T31, X49), SCOPE: 4, CLAUSE: 1\n\nT30 is ground\nT31 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(mult(T46, T47, X72), sum(X72, T46, X73))\n\nT46 is ground\nT47 is ground\nX73 is free\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: mult(T46, T47, X72)\n\nT46 is ground\nT47 is ground\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: sum(T50, T46, X73)\n\nT46 is ground\nT50 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: sum(T50, T46, X73), SCOPE: 5, CLAUSE: 2 | sum(T50, T46, X73), SCOPE: 5, CLAUSE: 3\n\nT46 is ground\nT50 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: sum(T50, T46, X73), SCOPE: 5, CLAUSE: 2\n\nT46 is ground\nT50 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: sum(T50, T46, X73), SCOPE: 5, CLAUSE: 3\n\nT46 is ground\nT50 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: sum(T64, T65, X96)\n\nT64 is ground\nT65 is ground\nX96 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: sum(T34, T30, X50)\n\nT30 is ground\nT34 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: sum(T70, T30, T13)\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: sum(T70, T30, T13), SCOPE: 6, CLAUSE: 2 | sum(T70, T30, T13), SCOPE: 6, CLAUSE: 3\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: sum(T70, T30, T13), SCOPE: 6, CLAUSE: 2\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: sum(T70, T30, T13), SCOPE: 6, CLAUSE: 3\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: sum(T86, T87, T89)\n\nT86 is ground\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 54 [arrowhead = none ];
54 -> 2;

55 [label="EVAL with clause\nmult(X3, 0, 0).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> 0,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 55 [arrowhead = none ];
55 -> 3;

56 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 56 [arrowhead = none ];
56 -> 4;

57 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 57 [arrowhead = none ];
57 -> 5;

58 [label="EVAL with clause\nmult(X10, s(X11), X12) :- ','(mult(X10, X11, X13), sum(X13, X10, X12)).\nand substitutionT1 -> T10,\nX10 -> T10,\nX11 -> T11,\nT2 -> s(T11),\nT3 -> T13,\nX12 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 58 [arrowhead = none ];
58 -> 7;

59 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 59 [arrowhead = none ];
59 -> 8;

60 [label="BACKTRACK\nfor clause: mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 60 [arrowhead = none ];
60 -> 6;

61 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 61 [arrowhead = none ];
61 -> 9;

62 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 62 [arrowhead = none ];
62 -> 10;

63 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 63 [arrowhead = none ];
63 -> 11;

64 [label="EVAL with clause\nmult(X18, 0, 0).\nand substitutionT10 -> T18,\nX18 -> T18,\nT11 -> 0,\nX13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 64 [arrowhead = none ];
64 -> 12;

65 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 65 [arrowhead = none ];
65 -> 13;

66 [label="EVAL with clause\nmult(X46, s(X47), X48) :- ','(mult(X46, X47, X49), sum(X49, X46, X48)).\nand substitutionT10 -> T30,\nX46 -> T30,\nX47 -> T31,\nT11 -> s(T31),\nX13 -> X50,\nX48 -> X50", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 66 [arrowhead = none ];
66 -> 22;

67 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 67 [arrowhead = none ];
67 -> 23;

68 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 68 [arrowhead = none ];
68 -> 14;

69 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 69 [arrowhead = none ];
69 -> 15;

70 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 70 [arrowhead = none ];
70 -> 16;

71 [label="EVAL with clause\nsum(X25, 0, X25).\nand substitutionX25 -> 0,\nT18 -> 0,\nT13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 71 [arrowhead = none ];
71 -> 17;

72 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 72 [arrowhead = none ];
72 -> 18;

73 [label="EVAL with clause\nsum(X32, s(X33), s(X34)) :- sum(X32, X33, X34).\nand substitutionX32 -> 0,\nX33 -> T23,\nT18 -> s(T23),\nX34 -> T25,\nT13 -> s(T25),\nT24 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 73 [arrowhead = none ];
73 -> 20;

74 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 74 [arrowhead = none ];
74 -> 21;

75 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 75 [arrowhead = none ];
75 -> 19;

76 [label="INSTANCE with matching:\nT18 -> T23\nT13 -> T25", fontsize=14, style = filled, fillcolor = lightgrey];
20 -> 76 [arrowhead = none , style=dashed];
76 -> 12[style=dashed];

77 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
22 -> 77 [arrowhead = none ];
77 -> 24;

78 [label="SPLIT 2\nnew knowledge:\nT30 is ground\nT31 is ground\nT34 is ground\nreplacements:X49 -> T34", fontsize=14, style = filled, fillcolor = violet];
22 -> 78 [arrowhead = none ];
78 -> 25;

79 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
24 -> 79 [arrowhead = none ];
79 -> 26;

80 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
25 -> 80 [arrowhead = none ];
80 -> 44;

81 [label="SPLIT 2\nnew knowledge:\nT34 is ground\nT30 is ground\nT70 is ground\nreplacements:X50 -> T70", fontsize=14, style = filled, fillcolor = violet];
25 -> 81 [arrowhead = none ];
81 -> 45;

82 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 82 [arrowhead = none ];
82 -> 27;

83 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 83 [arrowhead = none ];
83 -> 28;

84 [label="EVAL with clause\nmult(X59, 0, 0).\nand substitutionT30 -> T41,\nX59 -> T41,\nT31 -> 0,\nX49 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 84 [arrowhead = none ];
84 -> 29;

85 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 85 [arrowhead = none ];
85 -> 30;

86 [label="EVAL with clause\nmult(X69, s(X70), X71) :- ','(mult(X69, X70, X72), sum(X72, X69, X71)).\nand substitutionT30 -> T46,\nX69 -> T46,\nX70 -> T47,\nT31 -> s(T47),\nX49 -> X73,\nX71 -> X73", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 86 [arrowhead = none ];
86 -> 32;

87 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 87 [arrowhead = none ];
87 -> 33;

88 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 88 [arrowhead = none ];
88 -> 31;

89 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
32 -> 89 [arrowhead = none ];
89 -> 34;

90 [label="SPLIT 2\nnew knowledge:\nT46 is ground\nT47 is ground\nT50 is ground\nreplacements:X72 -> T50", fontsize=14, style = filled, fillcolor = violet];
32 -> 90 [arrowhead = none ];
90 -> 35;

91 [label="INSTANCE with matching:\nT30 -> T46\nT31 -> T47\nX49 -> X72", fontsize=14, style = filled, fillcolor = lightgrey];
34 -> 91 [arrowhead = none , style=dashed];
91 -> 24[style=dashed];

92 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 92 [arrowhead = none ];
92 -> 36;

93 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 93 [arrowhead = none ];
93 -> 37;

94 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 94 [arrowhead = none ];
94 -> 38;

95 [label="EVAL with clause\nsum(X84, 0, X84).\nand substitutionT50 -> T59,\nX84 -> T59,\nT46 -> 0,\nX73 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 95 [arrowhead = none ];
95 -> 39;

96 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 96 [arrowhead = none ];
96 -> 40;

97 [label="EVAL with clause\nsum(X93, s(X94), s(X95)) :- sum(X93, X94, X95).\nand substitutionT50 -> T64,\nX93 -> T64,\nX94 -> T65,\nT46 -> s(T65),\nX95 -> X96,\nX73 -> s(X96)", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 97 [arrowhead = none ];
97 -> 42;

98 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 98 [arrowhead = none ];
98 -> 43;

99 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 99 [arrowhead = none ];
99 -> 41;

100 [label="INSTANCE with matching:\nT50 -> T64\nT46 -> T65\nX73 -> X96", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 100 [arrowhead = none , style=dashed];
100 -> 35[style=dashed];

101 [label="INSTANCE with matching:\nT50 -> T34\nT46 -> T30\nX73 -> X50", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 101 [arrowhead = none , style=dashed];
101 -> 35[style=dashed];

102 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
45 -> 102 [arrowhead = none ];
102 -> 46;

103 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
46 -> 103 [arrowhead = none ];
103 -> 47;

104 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
46 -> 104 [arrowhead = none ];
104 -> 48;

105 [label="EVAL with clause\nsum(X109, 0, X109).\nand substitutionT70 -> T79,\nX109 -> T79,\nT30 -> 0,\nT13 -> T79", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 105 [arrowhead = none ];
105 -> 49;

106 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 106 [arrowhead = none ];
106 -> 50;

107 [label="EVAL with clause\nsum(X116, s(X117), s(X118)) :- sum(X116, X117, X118).\nand substitutionT70 -> T86,\nX116 -> T86,\nX117 -> T87,\nT30 -> s(T87),\nX118 -> T89,\nT13 -> s(T89),\nT88 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 107 [arrowhead = none ];
107 -> 52;

108 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 108 [arrowhead = none ];
108 -> 53;

109 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 109 [arrowhead = none ];
109 -> 51;

110 [label="INSTANCE with matching:\nT70 -> T86\nT30 -> T87\nT13 -> T89", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 110 [arrowhead = none , style=dashed];
110 -> 45[style=dashed];

}

(2) Obligation:

Clauses:

sumA(0, 0).
sumA(s(T23), s(T25)) :- sumA(T23, T25).
multB(T41, 0, 0).
multB(T46, s(T47), X73) :- multB(T46, T47, X72).
multB(T46, s(T47), X73) :- ','(multB(T46, T47, T50), sumC(T50, T46, X73)).
sumC(T59, 0, T59).
sumC(T64, s(T65), s(X96)) :- sumC(T64, T65, X96).
sumD(T79, 0, T79).
sumD(T86, s(T87), s(T89)) :- sumD(T86, T87, T89).
multE(T5, 0, 0).
multE(T18, s(0), T13) :- sumA(T18, T13).
multE(T30, s(s(T31)), T13) :- multB(T30, T31, X49).
multE(T30, s(s(T31)), T13) :- ','(multB(T30, T31, T34), sumC(T34, T30, X50)).
multE(T30, s(s(T31)), T13) :- ','(multB(T30, T31, T34), ','(sumC(T34, T30, T70), sumD(T70, T30, T13))).

Query: multE(g,g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
multE_in: (b,b,f)
sumA_in: (b,f)
multB_in: (b,b,f)
sumC_in: (f,b,f)
sumD_in: (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

multE_in_gga(T5, 0, 0) → multE_out_gga(T5, 0, 0)
multE_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sumA_in_ga(T18, T13))
sumA_in_ga(0, 0) → sumA_out_ga(0, 0)
sumA_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sumA_in_ga(T23, T25))
U1_ga(T23, T25, sumA_out_ga(T23, T25)) → sumA_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sumA_out_ga(T18, T13)) → multE_out_gga(T18, s(0), T13)
multE_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, multB_in_gga(T30, T31, X49))
multB_in_gga(T41, 0, 0) → multB_out_gga(T41, 0, 0)
multB_in_gga(T46, s(T47), X73) → U2_gga(T46, T47, X73, multB_in_gga(T46, T47, X72))
multB_in_gga(T46, s(T47), X73) → U3_gga(T46, T47, X73, multB_in_gga(T46, T47, T50))
U3_gga(T46, T47, X73, multB_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X73, sumC_in_aga(T50, T46, X73))
sumC_in_aga(T59, 0, T59) → sumC_out_aga(T59, 0, T59)
sumC_in_aga(T64, s(T65), s(X96)) → U5_aga(T64, T65, X96, sumC_in_aga(T64, T65, X96))
U5_aga(T64, T65, X96, sumC_out_aga(T64, T65, X96)) → sumC_out_aga(T64, s(T65), s(X96))
U4_gga(T46, T47, X73, sumC_out_aga(T50, T46, X73)) → multB_out_gga(T46, s(T47), X73)
U2_gga(T46, T47, X73, multB_out_gga(T46, T47, X72)) → multB_out_gga(T46, s(T47), X73)
U8_gga(T30, T31, T13, multB_out_gga(T30, T31, X49)) → multE_out_gga(T30, s(s(T31)), T13)
multE_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, multB_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sumC_in_aga(T34, T30, X50))
U10_gga(T30, T31, T13, sumC_out_aga(T34, T30, X50)) → multE_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sumC_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sumD_in_aga(T70, T30, T13))
sumD_in_aga(T79, 0, T79) → sumD_out_aga(T79, 0, T79)
sumD_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sumD_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sumD_out_aga(T86, T87, T89)) → sumD_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sumD_out_aga(T70, T30, T13)) → multE_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multE_in_gga(x1, x2, x3)  =  multE_in_gga(x1, x2)
0  =  0
multE_out_gga(x1, x2, x3)  =  multE_out_gga(x1, x2)
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
sumA_in_ga(x1, x2)  =  sumA_in_ga(x1)
sumA_out_ga(x1, x2)  =  sumA_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
sumC_in_aga(x1, x2, x3)  =  sumC_in_aga(x2)
sumC_out_aga(x1, x2, x3)  =  sumC_out_aga(x2)
U5_aga(x1, x2, x3, x4)  =  U5_aga(x2, x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
sumD_in_aga(x1, x2, x3)  =  sumD_in_aga(x2)
sumD_out_aga(x1, x2, x3)  =  sumD_out_aga(x2)
U6_aga(x1, x2, x3, x4)  =  U6_aga(x2, x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

multE_in_gga(T5, 0, 0) → multE_out_gga(T5, 0, 0)
multE_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sumA_in_ga(T18, T13))
sumA_in_ga(0, 0) → sumA_out_ga(0, 0)
sumA_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sumA_in_ga(T23, T25))
U1_ga(T23, T25, sumA_out_ga(T23, T25)) → sumA_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sumA_out_ga(T18, T13)) → multE_out_gga(T18, s(0), T13)
multE_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, multB_in_gga(T30, T31, X49))
multB_in_gga(T41, 0, 0) → multB_out_gga(T41, 0, 0)
multB_in_gga(T46, s(T47), X73) → U2_gga(T46, T47, X73, multB_in_gga(T46, T47, X72))
multB_in_gga(T46, s(T47), X73) → U3_gga(T46, T47, X73, multB_in_gga(T46, T47, T50))
U3_gga(T46, T47, X73, multB_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X73, sumC_in_aga(T50, T46, X73))
sumC_in_aga(T59, 0, T59) → sumC_out_aga(T59, 0, T59)
sumC_in_aga(T64, s(T65), s(X96)) → U5_aga(T64, T65, X96, sumC_in_aga(T64, T65, X96))
U5_aga(T64, T65, X96, sumC_out_aga(T64, T65, X96)) → sumC_out_aga(T64, s(T65), s(X96))
U4_gga(T46, T47, X73, sumC_out_aga(T50, T46, X73)) → multB_out_gga(T46, s(T47), X73)
U2_gga(T46, T47, X73, multB_out_gga(T46, T47, X72)) → multB_out_gga(T46, s(T47), X73)
U8_gga(T30, T31, T13, multB_out_gga(T30, T31, X49)) → multE_out_gga(T30, s(s(T31)), T13)
multE_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, multB_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sumC_in_aga(T34, T30, X50))
U10_gga(T30, T31, T13, sumC_out_aga(T34, T30, X50)) → multE_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sumC_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sumD_in_aga(T70, T30, T13))
sumD_in_aga(T79, 0, T79) → sumD_out_aga(T79, 0, T79)
sumD_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sumD_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sumD_out_aga(T86, T87, T89)) → sumD_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sumD_out_aga(T70, T30, T13)) → multE_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multE_in_gga(x1, x2, x3)  =  multE_in_gga(x1, x2)
0  =  0
multE_out_gga(x1, x2, x3)  =  multE_out_gga(x1, x2)
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
sumA_in_ga(x1, x2)  =  sumA_in_ga(x1)
sumA_out_ga(x1, x2)  =  sumA_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
sumC_in_aga(x1, x2, x3)  =  sumC_in_aga(x2)
sumC_out_aga(x1, x2, x3)  =  sumC_out_aga(x2)
U5_aga(x1, x2, x3, x4)  =  U5_aga(x2, x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
sumD_in_aga(x1, x2, x3)  =  sumD_in_aga(x2)
sumD_out_aga(x1, x2, x3)  =  sumD_out_aga(x2)
U6_aga(x1, x2, x3, x4)  =  U6_aga(x2, x4)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

MULTE_IN_GGA(T18, s(0), T13) → U7_GGA(T18, T13, sumA_in_ga(T18, T13))
MULTE_IN_GGA(T18, s(0), T13) → SUMA_IN_GA(T18, T13)
SUMA_IN_GA(s(T23), s(T25)) → U1_GA(T23, T25, sumA_in_ga(T23, T25))
SUMA_IN_GA(s(T23), s(T25)) → SUMA_IN_GA(T23, T25)
MULTE_IN_GGA(T30, s(s(T31)), T13) → U8_GGA(T30, T31, T13, multB_in_gga(T30, T31, X49))
MULTE_IN_GGA(T30, s(s(T31)), T13) → MULTB_IN_GGA(T30, T31, X49)
MULTB_IN_GGA(T46, s(T47), X73) → U2_GGA(T46, T47, X73, multB_in_gga(T46, T47, X72))
MULTB_IN_GGA(T46, s(T47), X73) → MULTB_IN_GGA(T46, T47, X72)
MULTB_IN_GGA(T46, s(T47), X73) → U3_GGA(T46, T47, X73, multB_in_gga(T46, T47, T50))
U3_GGA(T46, T47, X73, multB_out_gga(T46, T47, T50)) → U4_GGA(T46, T47, X73, sumC_in_aga(T50, T46, X73))
U3_GGA(T46, T47, X73, multB_out_gga(T46, T47, T50)) → SUMC_IN_AGA(T50, T46, X73)
SUMC_IN_AGA(T64, s(T65), s(X96)) → U5_AGA(T64, T65, X96, sumC_in_aga(T64, T65, X96))
SUMC_IN_AGA(T64, s(T65), s(X96)) → SUMC_IN_AGA(T64, T65, X96)
MULTE_IN_GGA(T30, s(s(T31)), T13) → U9_GGA(T30, T31, T13, multB_in_gga(T30, T31, T34))
U9_GGA(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U10_GGA(T30, T31, T13, sumC_in_aga(T34, T30, X50))
U9_GGA(T30, T31, T13, multB_out_gga(T30, T31, T34)) → SUMC_IN_AGA(T34, T30, X50)
U9_GGA(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U11_GGA(T30, T31, T13, sumC_in_aga(T34, T30, T70))
U11_GGA(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → U12_GGA(T30, T31, T13, sumD_in_aga(T70, T30, T13))
U11_GGA(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → SUMD_IN_AGA(T70, T30, T13)
SUMD_IN_AGA(T86, s(T87), s(T89)) → U6_AGA(T86, T87, T89, sumD_in_aga(T86, T87, T89))
SUMD_IN_AGA(T86, s(T87), s(T89)) → SUMD_IN_AGA(T86, T87, T89)

The TRS R consists of the following rules:

multE_in_gga(T5, 0, 0) → multE_out_gga(T5, 0, 0)
multE_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sumA_in_ga(T18, T13))
sumA_in_ga(0, 0) → sumA_out_ga(0, 0)
sumA_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sumA_in_ga(T23, T25))
U1_ga(T23, T25, sumA_out_ga(T23, T25)) → sumA_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sumA_out_ga(T18, T13)) → multE_out_gga(T18, s(0), T13)
multE_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, multB_in_gga(T30, T31, X49))
multB_in_gga(T41, 0, 0) → multB_out_gga(T41, 0, 0)
multB_in_gga(T46, s(T47), X73) → U2_gga(T46, T47, X73, multB_in_gga(T46, T47, X72))
multB_in_gga(T46, s(T47), X73) → U3_gga(T46, T47, X73, multB_in_gga(T46, T47, T50))
U3_gga(T46, T47, X73, multB_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X73, sumC_in_aga(T50, T46, X73))
sumC_in_aga(T59, 0, T59) → sumC_out_aga(T59, 0, T59)
sumC_in_aga(T64, s(T65), s(X96)) → U5_aga(T64, T65, X96, sumC_in_aga(T64, T65, X96))
U5_aga(T64, T65, X96, sumC_out_aga(T64, T65, X96)) → sumC_out_aga(T64, s(T65), s(X96))
U4_gga(T46, T47, X73, sumC_out_aga(T50, T46, X73)) → multB_out_gga(T46, s(T47), X73)
U2_gga(T46, T47, X73, multB_out_gga(T46, T47, X72)) → multB_out_gga(T46, s(T47), X73)
U8_gga(T30, T31, T13, multB_out_gga(T30, T31, X49)) → multE_out_gga(T30, s(s(T31)), T13)
multE_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, multB_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sumC_in_aga(T34, T30, X50))
U10_gga(T30, T31, T13, sumC_out_aga(T34, T30, X50)) → multE_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sumC_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sumD_in_aga(T70, T30, T13))
sumD_in_aga(T79, 0, T79) → sumD_out_aga(T79, 0, T79)
sumD_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sumD_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sumD_out_aga(T86, T87, T89)) → sumD_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sumD_out_aga(T70, T30, T13)) → multE_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multE_in_gga(x1, x2, x3)  =  multE_in_gga(x1, x2)
0  =  0
multE_out_gga(x1, x2, x3)  =  multE_out_gga(x1, x2)
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
sumA_in_ga(x1, x2)  =  sumA_in_ga(x1)
sumA_out_ga(x1, x2)  =  sumA_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
sumC_in_aga(x1, x2, x3)  =  sumC_in_aga(x2)
sumC_out_aga(x1, x2, x3)  =  sumC_out_aga(x2)
U5_aga(x1, x2, x3, x4)  =  U5_aga(x2, x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
sumD_in_aga(x1, x2, x3)  =  sumD_in_aga(x2)
sumD_out_aga(x1, x2, x3)  =  sumD_out_aga(x2)
U6_aga(x1, x2, x3, x4)  =  U6_aga(x2, x4)
MULTE_IN_GGA(x1, x2, x3)  =  MULTE_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
SUMA_IN_GA(x1, x2)  =  SUMA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
SUMC_IN_AGA(x1, x2, x3)  =  SUMC_IN_AGA(x2)
U5_AGA(x1, x2, x3, x4)  =  U5_AGA(x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
SUMD_IN_AGA(x1, x2, x3)  =  SUMD_IN_AGA(x2)
U6_AGA(x1, x2, x3, x4)  =  U6_AGA(x2, x4)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTE_IN_GGA(T18, s(0), T13) → U7_GGA(T18, T13, sumA_in_ga(T18, T13))
MULTE_IN_GGA(T18, s(0), T13) → SUMA_IN_GA(T18, T13)
SUMA_IN_GA(s(T23), s(T25)) → U1_GA(T23, T25, sumA_in_ga(T23, T25))
SUMA_IN_GA(s(T23), s(T25)) → SUMA_IN_GA(T23, T25)
MULTE_IN_GGA(T30, s(s(T31)), T13) → U8_GGA(T30, T31, T13, multB_in_gga(T30, T31, X49))
MULTE_IN_GGA(T30, s(s(T31)), T13) → MULTB_IN_GGA(T30, T31, X49)
MULTB_IN_GGA(T46, s(T47), X73) → U2_GGA(T46, T47, X73, multB_in_gga(T46, T47, X72))
MULTB_IN_GGA(T46, s(T47), X73) → MULTB_IN_GGA(T46, T47, X72)
MULTB_IN_GGA(T46, s(T47), X73) → U3_GGA(T46, T47, X73, multB_in_gga(T46, T47, T50))
U3_GGA(T46, T47, X73, multB_out_gga(T46, T47, T50)) → U4_GGA(T46, T47, X73, sumC_in_aga(T50, T46, X73))
U3_GGA(T46, T47, X73, multB_out_gga(T46, T47, T50)) → SUMC_IN_AGA(T50, T46, X73)
SUMC_IN_AGA(T64, s(T65), s(X96)) → U5_AGA(T64, T65, X96, sumC_in_aga(T64, T65, X96))
SUMC_IN_AGA(T64, s(T65), s(X96)) → SUMC_IN_AGA(T64, T65, X96)
MULTE_IN_GGA(T30, s(s(T31)), T13) → U9_GGA(T30, T31, T13, multB_in_gga(T30, T31, T34))
U9_GGA(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U10_GGA(T30, T31, T13, sumC_in_aga(T34, T30, X50))
U9_GGA(T30, T31, T13, multB_out_gga(T30, T31, T34)) → SUMC_IN_AGA(T34, T30, X50)
U9_GGA(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U11_GGA(T30, T31, T13, sumC_in_aga(T34, T30, T70))
U11_GGA(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → U12_GGA(T30, T31, T13, sumD_in_aga(T70, T30, T13))
U11_GGA(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → SUMD_IN_AGA(T70, T30, T13)
SUMD_IN_AGA(T86, s(T87), s(T89)) → U6_AGA(T86, T87, T89, sumD_in_aga(T86, T87, T89))
SUMD_IN_AGA(T86, s(T87), s(T89)) → SUMD_IN_AGA(T86, T87, T89)

The TRS R consists of the following rules:

multE_in_gga(T5, 0, 0) → multE_out_gga(T5, 0, 0)
multE_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sumA_in_ga(T18, T13))
sumA_in_ga(0, 0) → sumA_out_ga(0, 0)
sumA_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sumA_in_ga(T23, T25))
U1_ga(T23, T25, sumA_out_ga(T23, T25)) → sumA_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sumA_out_ga(T18, T13)) → multE_out_gga(T18, s(0), T13)
multE_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, multB_in_gga(T30, T31, X49))
multB_in_gga(T41, 0, 0) → multB_out_gga(T41, 0, 0)
multB_in_gga(T46, s(T47), X73) → U2_gga(T46, T47, X73, multB_in_gga(T46, T47, X72))
multB_in_gga(T46, s(T47), X73) → U3_gga(T46, T47, X73, multB_in_gga(T46, T47, T50))
U3_gga(T46, T47, X73, multB_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X73, sumC_in_aga(T50, T46, X73))
sumC_in_aga(T59, 0, T59) → sumC_out_aga(T59, 0, T59)
sumC_in_aga(T64, s(T65), s(X96)) → U5_aga(T64, T65, X96, sumC_in_aga(T64, T65, X96))
U5_aga(T64, T65, X96, sumC_out_aga(T64, T65, X96)) → sumC_out_aga(T64, s(T65), s(X96))
U4_gga(T46, T47, X73, sumC_out_aga(T50, T46, X73)) → multB_out_gga(T46, s(T47), X73)
U2_gga(T46, T47, X73, multB_out_gga(T46, T47, X72)) → multB_out_gga(T46, s(T47), X73)
U8_gga(T30, T31, T13, multB_out_gga(T30, T31, X49)) → multE_out_gga(T30, s(s(T31)), T13)
multE_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, multB_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sumC_in_aga(T34, T30, X50))
U10_gga(T30, T31, T13, sumC_out_aga(T34, T30, X50)) → multE_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sumC_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sumD_in_aga(T70, T30, T13))
sumD_in_aga(T79, 0, T79) → sumD_out_aga(T79, 0, T79)
sumD_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sumD_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sumD_out_aga(T86, T87, T89)) → sumD_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sumD_out_aga(T70, T30, T13)) → multE_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multE_in_gga(x1, x2, x3)  =  multE_in_gga(x1, x2)
0  =  0
multE_out_gga(x1, x2, x3)  =  multE_out_gga(x1, x2)
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
sumA_in_ga(x1, x2)  =  sumA_in_ga(x1)
sumA_out_ga(x1, x2)  =  sumA_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
sumC_in_aga(x1, x2, x3)  =  sumC_in_aga(x2)
sumC_out_aga(x1, x2, x3)  =  sumC_out_aga(x2)
U5_aga(x1, x2, x3, x4)  =  U5_aga(x2, x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
sumD_in_aga(x1, x2, x3)  =  sumD_in_aga(x2)
sumD_out_aga(x1, x2, x3)  =  sumD_out_aga(x2)
U6_aga(x1, x2, x3, x4)  =  U6_aga(x2, x4)
MULTE_IN_GGA(x1, x2, x3)  =  MULTE_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
SUMA_IN_GA(x1, x2)  =  SUMA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
SUMC_IN_AGA(x1, x2, x3)  =  SUMC_IN_AGA(x2)
U5_AGA(x1, x2, x3, x4)  =  U5_AGA(x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
SUMD_IN_AGA(x1, x2, x3)  =  SUMD_IN_AGA(x2)
U6_AGA(x1, x2, x3, x4)  =  U6_AGA(x2, x4)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 17 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMD_IN_AGA(T86, s(T87), s(T89)) → SUMD_IN_AGA(T86, T87, T89)

The TRS R consists of the following rules:

multE_in_gga(T5, 0, 0) → multE_out_gga(T5, 0, 0)
multE_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sumA_in_ga(T18, T13))
sumA_in_ga(0, 0) → sumA_out_ga(0, 0)
sumA_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sumA_in_ga(T23, T25))
U1_ga(T23, T25, sumA_out_ga(T23, T25)) → sumA_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sumA_out_ga(T18, T13)) → multE_out_gga(T18, s(0), T13)
multE_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, multB_in_gga(T30, T31, X49))
multB_in_gga(T41, 0, 0) → multB_out_gga(T41, 0, 0)
multB_in_gga(T46, s(T47), X73) → U2_gga(T46, T47, X73, multB_in_gga(T46, T47, X72))
multB_in_gga(T46, s(T47), X73) → U3_gga(T46, T47, X73, multB_in_gga(T46, T47, T50))
U3_gga(T46, T47, X73, multB_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X73, sumC_in_aga(T50, T46, X73))
sumC_in_aga(T59, 0, T59) → sumC_out_aga(T59, 0, T59)
sumC_in_aga(T64, s(T65), s(X96)) → U5_aga(T64, T65, X96, sumC_in_aga(T64, T65, X96))
U5_aga(T64, T65, X96, sumC_out_aga(T64, T65, X96)) → sumC_out_aga(T64, s(T65), s(X96))
U4_gga(T46, T47, X73, sumC_out_aga(T50, T46, X73)) → multB_out_gga(T46, s(T47), X73)
U2_gga(T46, T47, X73, multB_out_gga(T46, T47, X72)) → multB_out_gga(T46, s(T47), X73)
U8_gga(T30, T31, T13, multB_out_gga(T30, T31, X49)) → multE_out_gga(T30, s(s(T31)), T13)
multE_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, multB_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sumC_in_aga(T34, T30, X50))
U10_gga(T30, T31, T13, sumC_out_aga(T34, T30, X50)) → multE_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sumC_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sumD_in_aga(T70, T30, T13))
sumD_in_aga(T79, 0, T79) → sumD_out_aga(T79, 0, T79)
sumD_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sumD_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sumD_out_aga(T86, T87, T89)) → sumD_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sumD_out_aga(T70, T30, T13)) → multE_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multE_in_gga(x1, x2, x3)  =  multE_in_gga(x1, x2)
0  =  0
multE_out_gga(x1, x2, x3)  =  multE_out_gga(x1, x2)
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
sumA_in_ga(x1, x2)  =  sumA_in_ga(x1)
sumA_out_ga(x1, x2)  =  sumA_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
sumC_in_aga(x1, x2, x3)  =  sumC_in_aga(x2)
sumC_out_aga(x1, x2, x3)  =  sumC_out_aga(x2)
U5_aga(x1, x2, x3, x4)  =  U5_aga(x2, x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
sumD_in_aga(x1, x2, x3)  =  sumD_in_aga(x2)
sumD_out_aga(x1, x2, x3)  =  sumD_out_aga(x2)
U6_aga(x1, x2, x3, x4)  =  U6_aga(x2, x4)
SUMD_IN_AGA(x1, x2, x3)  =  SUMD_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMD_IN_AGA(T86, s(T87), s(T89)) → SUMD_IN_AGA(T86, T87, T89)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUMD_IN_AGA(x1, x2, x3)  =  SUMD_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUMD_IN_AGA(s(T87)) → SUMD_IN_AGA(T87)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• SUMD_IN_AGA(s(T87)) → SUMD_IN_AGA(T87)
  The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMC_IN_AGA(T64, s(T65), s(X96)) → SUMC_IN_AGA(T64, T65, X96)

The TRS R consists of the following rules:

multE_in_gga(T5, 0, 0) → multE_out_gga(T5, 0, 0)
multE_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sumA_in_ga(T18, T13))
sumA_in_ga(0, 0) → sumA_out_ga(0, 0)
sumA_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sumA_in_ga(T23, T25))
U1_ga(T23, T25, sumA_out_ga(T23, T25)) → sumA_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sumA_out_ga(T18, T13)) → multE_out_gga(T18, s(0), T13)
multE_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, multB_in_gga(T30, T31, X49))
multB_in_gga(T41, 0, 0) → multB_out_gga(T41, 0, 0)
multB_in_gga(T46, s(T47), X73) → U2_gga(T46, T47, X73, multB_in_gga(T46, T47, X72))
multB_in_gga(T46, s(T47), X73) → U3_gga(T46, T47, X73, multB_in_gga(T46, T47, T50))
U3_gga(T46, T47, X73, multB_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X73, sumC_in_aga(T50, T46, X73))
sumC_in_aga(T59, 0, T59) → sumC_out_aga(T59, 0, T59)
sumC_in_aga(T64, s(T65), s(X96)) → U5_aga(T64, T65, X96, sumC_in_aga(T64, T65, X96))
U5_aga(T64, T65, X96, sumC_out_aga(T64, T65, X96)) → sumC_out_aga(T64, s(T65), s(X96))
U4_gga(T46, T47, X73, sumC_out_aga(T50, T46, X73)) → multB_out_gga(T46, s(T47), X73)
U2_gga(T46, T47, X73, multB_out_gga(T46, T47, X72)) → multB_out_gga(T46, s(T47), X73)
U8_gga(T30, T31, T13, multB_out_gga(T30, T31, X49)) → multE_out_gga(T30, s(s(T31)), T13)
multE_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, multB_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sumC_in_aga(T34, T30, X50))
U10_gga(T30, T31, T13, sumC_out_aga(T34, T30, X50)) → multE_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sumC_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sumD_in_aga(T70, T30, T13))
sumD_in_aga(T79, 0, T79) → sumD_out_aga(T79, 0, T79)
sumD_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sumD_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sumD_out_aga(T86, T87, T89)) → sumD_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sumD_out_aga(T70, T30, T13)) → multE_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multE_in_gga(x1, x2, x3)  =  multE_in_gga(x1, x2)
0  =  0
multE_out_gga(x1, x2, x3)  =  multE_out_gga(x1, x2)
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
sumA_in_ga(x1, x2)  =  sumA_in_ga(x1)
sumA_out_ga(x1, x2)  =  sumA_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
sumC_in_aga(x1, x2, x3)  =  sumC_in_aga(x2)
sumC_out_aga(x1, x2, x3)  =  sumC_out_aga(x2)
U5_aga(x1, x2, x3, x4)  =  U5_aga(x2, x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
sumD_in_aga(x1, x2, x3)  =  sumD_in_aga(x2)
sumD_out_aga(x1, x2, x3)  =  sumD_out_aga(x2)
U6_aga(x1, x2, x3, x4)  =  U6_aga(x2, x4)
SUMC_IN_AGA(x1, x2, x3)  =  SUMC_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMC_IN_AGA(T64, s(T65), s(X96)) → SUMC_IN_AGA(T64, T65, X96)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUMC_IN_AGA(x1, x2, x3)  =  SUMC_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUMC_IN_AGA(s(T65)) → SUMC_IN_AGA(T65)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• SUMC_IN_AGA(s(T65)) → SUMC_IN_AGA(T65)
  The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTB_IN_GGA(T46, s(T47), X73) → MULTB_IN_GGA(T46, T47, X72)

The TRS R consists of the following rules:

multE_in_gga(T5, 0, 0) → multE_out_gga(T5, 0, 0)
multE_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sumA_in_ga(T18, T13))
sumA_in_ga(0, 0) → sumA_out_ga(0, 0)
sumA_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sumA_in_ga(T23, T25))
U1_ga(T23, T25, sumA_out_ga(T23, T25)) → sumA_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sumA_out_ga(T18, T13)) → multE_out_gga(T18, s(0), T13)
multE_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, multB_in_gga(T30, T31, X49))
multB_in_gga(T41, 0, 0) → multB_out_gga(T41, 0, 0)
multB_in_gga(T46, s(T47), X73) → U2_gga(T46, T47, X73, multB_in_gga(T46, T47, X72))
multB_in_gga(T46, s(T47), X73) → U3_gga(T46, T47, X73, multB_in_gga(T46, T47, T50))
U3_gga(T46, T47, X73, multB_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X73, sumC_in_aga(T50, T46, X73))
sumC_in_aga(T59, 0, T59) → sumC_out_aga(T59, 0, T59)
sumC_in_aga(T64, s(T65), s(X96)) → U5_aga(T64, T65, X96, sumC_in_aga(T64, T65, X96))
U5_aga(T64, T65, X96, sumC_out_aga(T64, T65, X96)) → sumC_out_aga(T64, s(T65), s(X96))
U4_gga(T46, T47, X73, sumC_out_aga(T50, T46, X73)) → multB_out_gga(T46, s(T47), X73)
U2_gga(T46, T47, X73, multB_out_gga(T46, T47, X72)) → multB_out_gga(T46, s(T47), X73)
U8_gga(T30, T31, T13, multB_out_gga(T30, T31, X49)) → multE_out_gga(T30, s(s(T31)), T13)
multE_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, multB_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sumC_in_aga(T34, T30, X50))
U10_gga(T30, T31, T13, sumC_out_aga(T34, T30, X50)) → multE_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sumC_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sumD_in_aga(T70, T30, T13))
sumD_in_aga(T79, 0, T79) → sumD_out_aga(T79, 0, T79)
sumD_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sumD_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sumD_out_aga(T86, T87, T89)) → sumD_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sumD_out_aga(T70, T30, T13)) → multE_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multE_in_gga(x1, x2, x3)  =  multE_in_gga(x1, x2)
0  =  0
multE_out_gga(x1, x2, x3)  =  multE_out_gga(x1, x2)
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
sumA_in_ga(x1, x2)  =  sumA_in_ga(x1)
sumA_out_ga(x1, x2)  =  sumA_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
sumC_in_aga(x1, x2, x3)  =  sumC_in_aga(x2)
sumC_out_aga(x1, x2, x3)  =  sumC_out_aga(x2)
U5_aga(x1, x2, x3, x4)  =  U5_aga(x2, x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
sumD_in_aga(x1, x2, x3)  =  sumD_in_aga(x2)
sumD_out_aga(x1, x2, x3)  =  sumD_out_aga(x2)
U6_aga(x1, x2, x3, x4)  =  U6_aga(x2, x4)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTB_IN_GGA(T46, s(T47), X73) → MULTB_IN_GGA(T46, T47, X72)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTB_IN_GGA(x1, x2, x3)  =  MULTB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTB_IN_GGA(T46, s(T47)) → MULTB_IN_GGA(T46, T47)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MULTB_IN_GGA(T46, s(T47)) → MULTB_IN_GGA(T46, T47)
  The graph contains the following edges 1 >= 1, 2 > 2

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMA_IN_GA(s(T23), s(T25)) → SUMA_IN_GA(T23, T25)

The TRS R consists of the following rules:

multE_in_gga(T5, 0, 0) → multE_out_gga(T5, 0, 0)
multE_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sumA_in_ga(T18, T13))
sumA_in_ga(0, 0) → sumA_out_ga(0, 0)
sumA_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sumA_in_ga(T23, T25))
U1_ga(T23, T25, sumA_out_ga(T23, T25)) → sumA_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sumA_out_ga(T18, T13)) → multE_out_gga(T18, s(0), T13)
multE_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, multB_in_gga(T30, T31, X49))
multB_in_gga(T41, 0, 0) → multB_out_gga(T41, 0, 0)
multB_in_gga(T46, s(T47), X73) → U2_gga(T46, T47, X73, multB_in_gga(T46, T47, X72))
multB_in_gga(T46, s(T47), X73) → U3_gga(T46, T47, X73, multB_in_gga(T46, T47, T50))
U3_gga(T46, T47, X73, multB_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X73, sumC_in_aga(T50, T46, X73))
sumC_in_aga(T59, 0, T59) → sumC_out_aga(T59, 0, T59)
sumC_in_aga(T64, s(T65), s(X96)) → U5_aga(T64, T65, X96, sumC_in_aga(T64, T65, X96))
U5_aga(T64, T65, X96, sumC_out_aga(T64, T65, X96)) → sumC_out_aga(T64, s(T65), s(X96))
U4_gga(T46, T47, X73, sumC_out_aga(T50, T46, X73)) → multB_out_gga(T46, s(T47), X73)
U2_gga(T46, T47, X73, multB_out_gga(T46, T47, X72)) → multB_out_gga(T46, s(T47), X73)
U8_gga(T30, T31, T13, multB_out_gga(T30, T31, X49)) → multE_out_gga(T30, s(s(T31)), T13)
multE_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, multB_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sumC_in_aga(T34, T30, X50))
U10_gga(T30, T31, T13, sumC_out_aga(T34, T30, X50)) → multE_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, multB_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sumC_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sumC_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sumD_in_aga(T70, T30, T13))
sumD_in_aga(T79, 0, T79) → sumD_out_aga(T79, 0, T79)
sumD_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sumD_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sumD_out_aga(T86, T87, T89)) → sumD_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sumD_out_aga(T70, T30, T13)) → multE_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multE_in_gga(x1, x2, x3)  =  multE_in_gga(x1, x2)
0  =  0
multE_out_gga(x1, x2, x3)  =  multE_out_gga(x1, x2)
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x1, x3)
sumA_in_ga(x1, x2)  =  sumA_in_ga(x1)
sumA_out_ga(x1, x2)  =  sumA_out_ga(x1, x2)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
multB_in_gga(x1, x2, x3)  =  multB_in_gga(x1, x2)
multB_out_gga(x1, x2, x3)  =  multB_out_gga(x1, x2)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
sumC_in_aga(x1, x2, x3)  =  sumC_in_aga(x2)
sumC_out_aga(x1, x2, x3)  =  sumC_out_aga(x2)
U5_aga(x1, x2, x3, x4)  =  U5_aga(x2, x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
sumD_in_aga(x1, x2, x3)  =  sumD_in_aga(x2)
sumD_out_aga(x1, x2, x3)  =  sumD_out_aga(x2)
U6_aga(x1, x2, x3, x4)  =  U6_aga(x2, x4)
SUMA_IN_GA(x1, x2)  =  SUMA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUMA_IN_GA(s(T23), s(T25)) → SUMA_IN_GA(T23, T25)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUMA_IN_GA(x1, x2)  =  SUMA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUMA_IN_GA(s(T23)) → SUMA_IN_GA(T23)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• SUMA_IN_GA(s(T23)) → SUMA_IN_GA(T23)
  The graph contains the following edges 1 > 1

(36) YES